; EXPECT: sat
(set-logic ALL)
(set-option :incremental false)
(declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero))((cons (car tree) (cdr list)) (null))((node (children list)) (leaf (data nat)))))
(declare-fun x1 () nat)
(declare-fun x2 () nat)
(declare-fun x3 () nat)
(declare-fun x4 () list)
(declare-fun x5 () list)
(declare-fun x6 () list)
(declare-fun x7 () tree)
(declare-fun x8 () tree)
(declare-fun x9 () tree)
(check-sat-assuming ( (not (not (and (and (and (and (and (not ((_ is succ) (pred (data (leaf x3))))) (= x1 zero)) (not ((_ is zero) (succ (succ zero))))) (not (= x3 x2))) (= x4 (cdr x5))) ((_ is cons) (cons x8 x5))))) ))
